$\forall$${\it es}$:ES, $e$:E, $l$:IdLnk, $L$:E List.
\\[0ex]rcvs from $e$ on $l$ = $L$
\\[0ex]$\Rightarrow$ ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $\exists$${\it e'}$:E. isrcv(${\it e'}$) \& lnk(${\it e'}$) $=$ $l$ \& sender(${\it e'}$) $=$ $e$ \& index(${\it e'}$) $=$ $i$ $\in$ $\mathbb{Z}$)